A Financial Computing System (FCS) is a computer system that can be used to make suggestions of what to trade given a certain criteria and that place or execute orders for financial products, such as stocks, bonds, derivatives, commodities, etc. Financial Computing Systems are prevalent in today's financial markets and a wide variety of stakeholders use them. Broker-dealers and market makers employ FCSs, for example, to execute orders on behalf of their clients and/or to automate decisions of capital commitment. Institutional investors, such as mutual and hedge funds, often use FCSs to implement custom trading algorithms to manage positions. High Frequency Traders (HFT) use electronic trading platforms to trade securities rapidly. Also, trading venues or platforms such as exchanges and ‘dark pools’, where orders/quotes are matched, employ financial computing systems to implement their matching and execution logic. The software for these trading systems automate decisions about financial transactions, such as what to trade and where, or how to match an order in the case of a trading venue. Yet this highly complex software must also adhere to applicable laws, regulations, and internal controls. There have been several incidents for FCS “glitches” and “bugs” that caused financial losses and/or embarrassment.
A significant challenge for regulators of FCSs (and those trading on them) is that the documentation and marketing materials describing the FCSs are often imprecise. The documentation is commonly expressed in English prose, which is a deficient way to communicate the behavior of complicated algorithms underlying FCSs. English descriptions of algorithms lead to ambiguity and open up opportunities for ‘liberal’ interpretations. But most importantly, English prose makes it impossible to automatically analyze algorithm behavior for compliance with regulatory directives, or to reconcile such descriptions with production systems. The lack of precisely described rules by which venues operate also obstructs their clients from thoroughly testing their systems' connectivity to those venues, making the process tedious and expensive.
Automated Theorem Proving (“ATP”) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems automatically by computer programs. It is often used in hardware (e.g., integrated circuits) and software design to verify that the designs are error-free (at least for certain types of errors). The application of ATP to mathematically verify properties of hardware and software designs is commonly referred to as “formal verification.”